(DEFPROP ATTEMPT 
 (LAMBDA(Z S C)
  (PROG (NEWNAME SUPPORT
 		 EDITSTRAT
 		 LCL
 		 LVL
 		 CNT
 		 XYZ2
 		 LSTCLS
 		 LLST
 		 Z1
 		 MERGE
 		 ORDER
 		 DEBUG
 		 DEPTH
 		 LENGTH
 		 ANCESTRY
 		 STRATEGY
 		 STRAT
 		 PMODEL
 		 NMODEL
 		 PFLG
 		 PDEPTH
 		 DLIST
 		 XYZ
 		 XYZ1
 		 COND
 		 UNAXP
 		 UNAXN
 		 SAT
 		 EE
 		 EE1
 		 XX
 		 CLAUSES
 		 SUBCLAUSES
 		 COUNT)
	(SETQ TBL (SET1 (APPEND PREFN INFN)))
	(SET3 Z)
	(SETQ Z (MINIMIZE Z))
	(SETQ CLAUSES Z)
	(SETQ NEWNAME (INITIAL Z))
	(UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
	(SETQ COND C)
	(SETQ XYZ2 Z)
	(SETQ LVL 1)
	(SETQ COUNT 0)
	(SETQ Z (UNITPN XYZ2))
	(SETQ UNAXP (CAR Z))
	(SETQ UNAXN (CDR Z))
	(SETQ CLAUSES XYZ2)
	(COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
			  (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
	      (T (SETQ SUBCLAUSES CLAUSES)))
	(SETQ LCL (LAST CLAUSES))
	(SETQ LSTCLS LCL)
	(COND (ANCESTRY (GO AA)))
	(SETQ XX (CONS CLAUSES CLAUSES))
	(SETQ EE CLAUSES)
	(SETQ EE1 (LAST EE))
	(SETQ CNT (LENGTH XYZ2))
   BB   (SETQ Z1 (ERRSET (ATTEMPT1 XYZ2)))
	(COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
	      ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
					       (EVAL
						(LIST (QUOTE OUTC)
						      (LIST (QUOTE OUTPUT)
							    (QUOTE PRF)
							    (QUOTE DSK:)
							    (CONS (READLIST
								   (CONS (QUOTE N)
									 (CONS (SETQ PRNO (ADD1 PRNO))
 									       FILENAM)))
								  (QUOTE PRF)))
 						      NIL)))
					 (QUERY)
					 (PROOF LHP RHP)
					 (OUTC Z T)
					 (RETURN Z1))
	      (T (RETURN Z1)))
   AA   (SETQ XYZ XYZ2)
	(SETQ EE CLAUSES)
	(SETQ EE1 (LAST CLAUSES))
   CC   (SETQ LLST (CONS (CAR XYZ) LLST))
	(SETQ XYZ (CDR XYZ))
	(COND (XYZ (GO CC)) (T (GO BB))))) 
EXPR)

(DEFPROP <MATCH> 
 (LAMBDA NIL
  (NLRR (QUOTE MATCH)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((<NUMBER>) (STK 0))
		((AND (<NOT1>) (<TM>)) (CONS (QUOTE %NG) (STK 0)))
		((AND (<TM>)) (STK 0))
		(*NIL*)))))) 
EXPR)